|
Independence-friendly logic (IF logic), proposed by Jaakko Hintikka and Gabriel Sandu in 1989, aims at being a more natural and intuitive alternative to classical first-order logic (FOL). IF logic is characterized by branching quantifiers. It is more expressive than FOL because it allows one to express independence relations between quantified variables. For example, the formula ∀a ∀b ∃c/b ∃d/a φ(a,b,c,d) ("x/y" should be read as "x independent of y") cannot be expressed in FOL. This is because c depends ''only'' on a and d depends ''only'' on b. First-order logic cannot express these independences by any linear reordering of the quantifiers. In part, IF logic was motivated by game semantics for games with imperfect information. IF logic is translation equivalent with existential second-order logic () and also with Väänänen's dependence logic and with first-order logic extended with Henkin quantifiers. Although it shares a number of metalogical properties with first-order logic, there are some differences, including lack of closure under negation and higher complexity for deciding the validity of formulas. Extended IF logic addresses the closure problem, but it sacrifices game semantics in the process, and it properly belongs to higher fragment of second-order logic ( ). Hintikka's proposal that IF logic and its extended version be used as foundations of mathematics has been met with skepticism by other mathematicians, including Väänänen and Solomon Feferman. == Semantics == Since Tarskian semantics does not allow indeterminate truth values, it cannot be used for IF logic. Hintikka further argues that the standard semantics of FOL cannot accommodate IF logic because the principle of compositionality fails in the latter. Wilfrid Hodges (1997) gives a compositional semantics for it in part by having the truth clauses for IF formulas quantify over sets of assignments rather than just assignments (as the usual truth clauses do). The game-theoretic semantics for FOL treats a FOL formula as a game of perfect information, whose players are Verifier and Falsifier. The same holds for the standard semantics of IF logic, except that the games are of imperfect information. Independence relations between the quantified variables are modelled in the game tree as indistinguishability relations between game states with respect to a certain player. In other words, the players are not certain where they are in the tree (this ignorance simulates simultaneous play). The formula is evaluated as true if there Verifier has a winning strategy, false if Falsifier has a winning strategy, and indeterminate otherwise. A winning strategy is informally defined as a strategy that is guaranteed to win the game, regardless of how the other players play. It can be given a completely rigorous, formal definition. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Independence-friendly logic」の詳細全文を読む スポンサード リンク
|